$\forall$$T$:Type, $P$:($L$:($T$ List)$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel-$1}}$$\rightarrow$Prop). Trans $1$,$2$:$T$ List. $1$ guarded\_permutation($T$;$P$) $2$